/**
 * @file matrice.h
 * @brief Matrice
 * @author Radim BADSI, Kévin CHAPON, Fanny FERLET
 */

#ifndef MATRICE_H
#define MATRICE_H

#define TAILLE_MATRICE_INIT 100000 /*!< Taille initiale de la matrice de stockage. */
#define COEF_AGRANDISSEMENT_MATRICE 2 /*!< Coefficient d'agrandissement de la matrice de stockage. */
#define NON_SIGNIFICATIF -1 /*!< Valeur non significative */


typedef int t_ptr_elem; /*!< Pointeur sur un élément. */

/**
 * Élément de la matrice
 */
typedef struct {
	int num_clause;				/*!< Numéro de la clause. */
	int num_variable;			/*!< Numéro de la varible. Son signe correspond au signe du littéral. */
	t_ptr_elem ptr_var_suiv;	/*!< Pointeur sur la prochaine occurence de la variable dans de la matrice. */
	t_ptr_elem ptr_clause_prec;	/*!< Pointeur sur le littéral précédent de la clause. */
	t_ptr_elem ptr_clause_suiv;	/*!< Pointeur sur le littéral suivant de la clause. */
} t_element;

/**
 * État d'une variable
 */
typedef enum {NEUTRE, VRAI, FAUX} t_etat_variable;

/**
 * État d'une clause
 */
typedef enum {SATISFAITE, INCHANGEE, RACCOURCIE} t_etat_clause;

/**
 * Littéral
 */
typedef struct {
	t_etat_variable etat;	/*!< Etat de la variable.*/
	t_ptr_elem ptr_premier;	/*!< Pointeur sur le premier élement dont la variable correspond au littéral. */
	t_ptr_elem ptr_dernier;	/*!< Pointeur sur la dernier élément inséré. */
	int nb_occ_pos;			/*!< Nombre d'occurrences positives. */
	int nb_occ_neg;			/*!< Nombre d'occurrences negatives. */
} t_litteral;

/**
 * Clause
 */
typedef struct {
	t_etat_clause etat;		/*!< Etat de la clause. */
	t_ptr_elem ptr_premier; /*!< Pointeur vers le premier élément de la clause. */
	t_ptr_elem ptr_dernier; /*!< Représente un pointeur sur le dernier élément inséré. */
} t_clause;

/**
 * Matrice de stockage
 */
typedef struct {
	t_element* elements;		/*!< Pointeur sur les éléments de la matrice. */
	int nb_elements;			/*!< Nombre d'éléments de la matrice. */
	int nb_clauses_a_traiter;	/*!< Nombre de clauses de la matrice. */
	int taille;					/*!< Taille de la matrice. */
} t_matrice;

/**
 * Calcule la valeur absolue d'un entier.
 * @param a entier
 * @return valeur absolu de l'entier.
 */
int abs (int a);

/**
 * Alloue l'espace nécessaire au stockage de la matrice
 * @param matrice Matrice
 */
void init_matrice (t_matrice* matrice);

/**
 * Agrandi la taille de la matrice
 * @param matrice Matrice
 */
void agrandir_matrice (t_matrice* matrice); 
 
/**
 * Adapte la taille de la mémoire allouée à la taille
 * de la matrice.
 * @param matrice matrice
 */
void reduire (t_matrice* matrice);
 
/**
    * Ajoute un élément à une matrice.
    * @param matrice matrice
    * @param tab_clauses tableau de variables
    * @param tab_variables tableau de clauses
    * @param num_clause numéro de la clause
    * @param num_variable numéro de la variable
    */
void ajouter (t_matrice* matrice,
			  t_clause* tab_clauses,
			  t_litteral* tab_variables,
			  int num_clause,
			  int num_variable
			  );

/**
	* Initialise des clauses.
	* Initialise les cases tab_clauses[1..tab_clauses[0]]=0.
	* @param nb_clauses nombre de clauses
	* @return Pointeur vers la zone mémoire allouée.
	*/
t_clause* init_clauses (int nb_clauses);

/**
 * Initialise les variables.
 * Initialise les cases tab_variables[1..tab_variables[0]]=0.
 * @param nb_litteraux nombre de littéraux
 * @return Pointeur vers la zone mémoire allouée.
 */
t_litteral* init_variables (int nb_litteraux);

/**
 * Teste si une clause est unitaire.
 * @param tab_clauses tableau de clauses
 * @param num_clause numéro de la clause concernée
 * @return Vrai si la clause est unitaire, faux sinon.
 */
int est_unitaire (t_clause* tab_clauses,
				  int num_clause
				 );

/**
 * Teste si une clause est marquée satisfaite.
 * @param tab_clauses tableau de clauses
 * @param num_clause numéro de la clause concernée
 * @return Vrai si la clause est marque satisfaite, faux sinon.
 */
int est_marque_satisfaite (t_clause* tab_clauses,
				  	 	   int num_clause
				 		  );

/**
 * Retourne le nombre de clauses.
 * @param tab_clauses tableau de clauses
 * @return Nombre de clauses.
 */			 		  
int nombre_clauses (t_clause* tab_clauses);

/**
 * Retourne le nombre de variables.
 * @param tab_variables tableau de variables
 * @return Nombre de variables.
 */			 	
int nombre_variables (t_litteral* tab_variables);

/**
 * Inidique si toutes les clauses sont satisfaites.
 * @param matrice matrice
 * @return Vrai si toutes les clauses sont satisfaites, faux sinon.
 */
int toutes_satisfaites (t_matrice* matrice);
#endif

